$\forall$$R$:Realizer, $i$:Id. $\neg$Rplus?($R$) $\Rightarrow$ $\neg$Rnone?($R$) $\Rightarrow$ R{-}has{-}loc($R$;$i$) $=$ R{-}loc($R$) = $i$ $\in$ $\mathbb{B}$